/*
 * SplittingTreeNode.cpp
 *
 * Copyright 2012 Fabian Wenzelmann
 *
 * This file is part of Recognition-Procedures-for-Boolean-Functions.
 *
 * Recognition-Procedures-for-Boolean-Functions is free software: you
 * can redistribute it and/or modify it under the terms of the
 * GNU General Public License as published by the Free Software Foundation,
 * either version 3 of the License, or (at your option) any later version.
 *
 * Recognition-Procedures-for-Boolean-Functions is distributed in the hope
 * that it will be useful, but WITHOUT ANY WARRANTY; without even the implied
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the GNU General
 * Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with Recognition-Procedures-for-Boolean-Functions.
 *
 * If not, see <http://www.gnu.org/licenses/>.
 */

#include "bfr/lpbCombinatorial/SplittingTreeNode.hpp"

namespace bfr {

void SplittingTreeNode::setUpperParent(SplittingTreeNode *up) {
    upperParent = up;
}

void SplittingTreeNode::setLowerParent(SplittingTreeNode *lp) {
    lowerParent = lp;
}

SplittingTreeNode::~SplittingTreeNode() {
    destroyContent(true);
}

SplittingTreeNode::SplittingTreeNode(SplittingTreeNode *lp,
        SplittingTreeNode *up,
        ClauseSet *d, std::vector<OccurrencePattern*> *o,
        TreeContext *c, SplittingNodeType t,
        const SplittingNodeContent &co) :
        lowerParent(lp), upperParent(up), lowerChild(NULL),
        upperChild(NULL), dnf(d), context(c), occurrences(o),
        setting(0), alreadySplit(false), type(t), content(co) {
    if (lowerParent != NULL) {
        column = lowerParent->getColumn() + 1;
    }
    else if (upperParent != NULL) {
        column = upperParent->getColumn() + 1;
    }
    else {
        column = 0;
    }
    if (context != NULL) {
        row = context->addNode(this);
    }
    else {
        row = -1;
    }
}

bool SplittingTreeNode::isFinal() const {
    if (type == SplittingNodeType::AUXILIARY_NODE)
        return false;
    return content.main.final;
}

SplittingTreeNode* SplittingTreeNode::getLowerParent() const {
    return lowerParent;
}

SplittingTreeNode* SplittingTreeNode::getUpperParent() const {
    return upperParent;
}

SplittingTreeNode* SplittingTreeNode::getLowerChild() const {
    return lowerChild;
}

SplittingTreeNode* SplittingTreeNode::getUpperChild() const {
    return upperChild;
}

ClauseSet* SplittingTreeNode::getDNF() const {
    return dnf;
}

size_t SplittingTreeNode::getColumn() const {
    return column;
}

size_t SplittingTreeNode::getRow() const {
    return row;
}

TreeContext* SplittingTreeNode::getContext() const {
    return context;
}

bool SplittingTreeNode::isAlreadySplit() const {
    return alreadySplit;
}

SplitResult SplittingTreeNode::splitAway(short k,
                       VariableSetting *variables,
                       bool createPatterns,
                       bool symmetryTest)
                throw (NotSymmetricException) {
    bool isResFinal = false;
    pattern_container_t *newOccurrences = NULL;
    if (createPatterns) {
        newOccurrences =
                new pattern_container_t(context->getVariableCount()-column-1,
                        NULL);
        //new pattern_container_t(occurrences->size() - 1, NULL);
    }
    // TODO: maybe use the old size?
    // or old size / 2, something like that?
    ClauseSet *newDNF = new ClauseSet();
    // TODO: different to the java version, but should be correct?
    if ((occurrences != NULL) && (occurrences->size() == 0)) {
        // TODO DEBUG
        std::cout << "WHAT???" << std::endl;
    }
    size_t variableID = variables->operator[](column);
    const Literal currentLiteral(variableID);
    if (k == 0) {
        // create new clause, actualize occurrence pattern for all copied variables
        ClauseSet::const_iterator e = dnf->end();
        for (ClauseSet::const_iterator it = dnf->begin();
                it != e;
                it++) {
            const Clause *c = *it;
            if (!(c->contains(currentLiteral))) {
                Clause *newClause = new Clause(c->size());
                Clause::const_iterator ce = c->end();
                for (Clause::const_iterator cit = c->begin();
                        cit != ce;
                        cit++) {
                    const Literal &l = *cit;
                    size_t lID = l.getId();
                    newClause->add(Literal(lID));

                    if (createPatterns) {
                        // get position of the variable
                        // in the global order
                        size_t pos = variables->getPos(lID);
                        OccurrencePattern *currOP =
                                newOccurrences
                                ->operator[](pos-column-1);
                        if (currOP == NULL) {
                            currOP = new OccurrencePattern(lID);
                            newOccurrences->operator[](pos-column-1) =
                                    currOP;
                        }
                        currOP->addOccurrence(c->size());
                    }

                }
                if (!newDNF->addSecure(newClause)) {
                    std::cout <<
                            "FIXME, created wrong occurrences";
                }
                if (newClause->size() == 0) {
                    isResFinal = true;
                }
            }
        }
    }
    else {
        // create new DNF but remove the variable
        ClauseSet::const_iterator e = dnf->end();
        for (ClauseSet::const_iterator it = dnf->begin();
                it != e;
                it++) {
            const Clause *c = *it;
            if (c->size() == 0) {
                // we found an empty clause. So return splitAway(0)
                delete newDNF;
                if (createPatterns) {
                    for (pattern_container_t::const_iterator pit =
                            newOccurrences->begin();
                            pit != newOccurrences->end(); pit++) {
                        delete *pit;
                    }
                    delete newOccurrences;
                }
                return splitAway(0, variables, createPatterns);
            }
            if (c->contains(currentLiteral)) {
                Clause *newClause = new Clause(c->size() - 1);
                Clause::const_iterator ce = c->end();
                for (Clause::const_iterator cit = c->begin();
                        cit != ce;
                        cit++) {
                    const Literal &l = *cit;
                    size_t lID = l.getId();
                    if (lID != variableID) {
                        // add this literal
                        newClause->add(Literal(lID));
                        if (createPatterns) {
                            // get position of the variable in the
                            // global order
                            size_t pos = variables->getPos(lID);
                            OccurrencePattern *currOP =
                                    newOccurrences
                                    ->operator[](pos-column-1);
                            if (currOP == NULL) {
                                currOP = new OccurrencePattern(lID);
                                newOccurrences->
                                operator[](pos-column-1) = currOP;
                            }
                            currOP->addOccurrence(c->size() - 1);
                        }
                    }
                }
                if (!newDNF->addSecure(newClause)) {
                    std::cout <<
                            "FIXME, created wrong occurrences";
                }
                if (newClause->size() == 0) {
                    isResFinal = true;
                }
            }
        }
    }
    if (newDNF->size() == 0) {
        isResFinal = true;
    }
    return SplitResult(isResFinal, newDNF, newOccurrences);
}

std::pair<SplitResult, SplitResult>
SplittingTreeNode::splitBoth(VariableSetting *variables,
        bool createPatterns, bool symmetryTest)
        throw (NotSymmetricException) {
    bool firstFinal = false;
    bool secondFinal = false;
    bool containsEmptyClause = false;
    pattern_container_t *firstOccurrences = NULL;
    pattern_container_t *secondOccurrences = NULL;
    if (createPatterns) {
        size_t newPatternSize = context->getVariableCount()-column-1;
        firstOccurrences = new pattern_container_t(newPatternSize,
                NULL);
        secondOccurrences = new pattern_container_t(newPatternSize,
                NULL);
    }
    if ((occurrences != NULL) && (occurrences->size() == 0)) {
        // TODO DEBUG
        std::cout << "WHAT???" << std::endl;
    }
    // TODO: maybe use the old size?
            // or old size / 2, something like that?
    ClauseSet *firstDNF = new ClauseSet();
    ClauseSet *secondDNF = new ClauseSet();
    size_t variableID = variables->operator[](column);
    // TODO: not nice, change design?
    const Literal currentLiteral(variableID);
    ClauseSet::const_iterator e = dnf->end();
    for (ClauseSet::const_iterator it = dnf->begin();
            it != e;
            it++) {
        const Clause *c = *it;
        if (c->size() == 0) {
            containsEmptyClause = true;
        }
        if (c->contains(currentLiteral)) {
            Clause *newClause = new Clause(c->size() - 1);
            Clause::const_iterator ce = c->end();
            for (Clause::const_iterator cit = c->begin();
                    cit != ce;
                    cit++) {
                const Literal &l = *cit;
                size_t lID = l.getId();
                if (lID != variableID) {
                    newClause->add(Literal(lID));
                    if (createPatterns) {
                        // get position of the variable in the
                        // global order
                        size_t pos = variables->getPos(lID);
                        OccurrencePattern *currOP =
                                secondOccurrences
                                ->operator[](pos-column-1);
                        if (currOP == NULL) {
                            currOP = new OccurrencePattern(lID);
                            secondOccurrences->
                            operator[](pos-column-1) = currOP;
                        }
                        currOP->addOccurrence(c->size() - 1);
                    }
                }
            }
            if (!secondDNF->addSecure(newClause)) {
                std::cout <<
                        "FIXME, created wrong occurrences";
            }
            if (newClause->size() == 0) {
                secondFinal = true;
            }
        }
        else {
            // copy the complete clause
            Clause *newClause = new Clause(c->size());
            Clause::const_iterator ce = c->end();

            for (Clause::const_iterator cit = c->begin();
                    cit != ce;
                    cit++) {
                const Literal &l = *cit;
                size_t lID = l.getId();
                newClause->add(Literal(lID));
                if (createPatterns) {
                    // get position of the variable in the
                    // global order
                    size_t pos = variables->getPos(lID);
                    OccurrencePattern *currOP =
                            firstOccurrences
                            ->operator[](pos-column-1);
                    if (currOP == NULL) {
                        currOP = new OccurrencePattern(lID);
                        firstOccurrences->
                        operator[](pos-column-1) = currOP;
                    }
                    currOP->addOccurrence(c->size());
                }
            }
            if (!firstDNF->addSecure(newClause)) {
                std::cout <<
                        "FIXME, created wrong occurrences";
            }
            if (newClause->size() == 0) {
                firstFinal = true;
            }
        }
    }
    if (firstDNF->size() == 0) {
        firstFinal = true;
    }

    if (secondDNF->size() == 0) {
        secondFinal = true;
    }

    // TODO: can we ever get here?
    if (containsEmptyClause) {
        // copy the first DNF, it appears in both results
        delete secondDNF;
        secondDNF = new ClauseSet(firstDNF->size());
        ClauseSet::const_iterator firstEnd = firstDNF->end();
        for (ClauseSet::const_iterator it = firstDNF->begin();
                it != firstEnd;
                it++) {
            const Clause *c = *it;
            Clause *newClause = new Clause(c->size());
            Clause::const_iterator clauseEnd = c->end();
            for (Clause::const_iterator cit = c->begin();
                    cit != clauseEnd;
                    cit++) {
                const Literal &l = *cit;
                newClause->add(Literal(l.getId()));
            }
            if (!secondDNF->addSecure(newClause)) {
                std::cout <<
                        "FIXME, created wrong occurrences";
            }
        }
        if (createPatterns) {
            // copy occurrences
            for (pattern_container_t::const_iterator it =
                    secondOccurrences->begin();
                    it != secondOccurrences->end();
                    it++) {
                delete *it;
            }
            delete secondOccurrences;
            secondOccurrences =
                    new pattern_container_t(firstOccurrences->size(),
                            NULL);
            size_t pPos = 0;
            for (pattern_container_t::const_iterator it =
                    firstOccurrences->begin();
                    it != firstOccurrences->end();
                    it++) {
                OccurrencePattern *p = *it;
                OccurrencePattern *newPattern =
                        new OccurrencePattern(*p);
                secondOccurrences->operator[](pPos++) = newPattern;
            }
        }
        secondFinal = firstFinal;
    }
    //SplitResult first = splitAway(0, opf, variables, cf, csf, createPatterns);
    //SplitResult second = splitAway(1, opf, variables, cf, csf, createPatterns);
    SplitResult first(firstFinal, firstDNF, firstOccurrences);
    SplitResult second(secondFinal, secondDNF, secondOccurrences);
    return std::pair<SplitResult, SplitResult>(first, second);
}

void SplittingTreeNode::destroyContent(bool delFirstOccurrences) {
    if ((column != 0) && (dnf != NULL)) {
        delete dnf;
        dnf = NULL;
    }
    if ((occurrences != NULL) &&
            ((column != 0) || delFirstOccurrences)) {
        for (pattern_container_t::const_iterator it = occurrences->begin();
             it != occurrences->end(); it++) {
            delete *it;
        }
        delete occurrences;
        occurrences = NULL;
    }
}

void SplittingTreeNode::calcIsFinal() {
    if(dnf->size() == 0) {
        content.main.final = true;
        return;
    }
    if(dnf->size() == 1) {
        if ((*(dnf->begin()))->size() == 0) {
            content.main.final = true;
            return;
        }
    }
    content.main.final = false;
}

size_t SplittingTreeNode::calcMaxL(VariableSetting *vs) const {
    size_t l = 1;
    // TODO: Strange behavior if the DNF cannot be represented as a LPB
    // first can be null in this case?
    // why? JGS: let's see if implementing a symmetry test will remedy this. 
    OccurrencePattern *first = occurrences->operator[](0);
    //if (first == NULL) std::cout << "first is NULL" << std::endl;//test line
    //std::cout << "occurrences->size() = " << occurrences->size() << std::endl;
    while(l < occurrences->size()) {
        OccurrencePattern *next = occurrences->operator[](l);
        if (next == NULL) {
            // TODO: create OP here with the right
            // variable ID
            // or is it wrong to do this?
            //std::cout << "NULL pattern" << std::endl;
            // TODO: correct?
            next = new OccurrencePattern(vs->operator[](column + l));
            occurrences->operator[](l) = next;
	    //std::cout << "reached occurrences->operator[](l) = next" << std::endl;
        }
	//std:: cout << "just before if(first->operator==(*next))" << std::endl;
	if (first == NULL) {//JGS: to fix the segmentation fault
	  l++;
	}
	else {
	  if (first->operator==(*next)) {
            l++;
	  }
	  else {
            break;
	  }
        }
	//std:: cout << "just after if(first->operator==(*next))" << std::endl;
    }
    return l;
}

bool SplittingTreeNode::createMainNode() const {
    return content.aux.lPrime == (content.aux.lValue - 1);
}

size_t SplittingTreeNode::getL() const {
    return content.aux.lValue;
}

size_t SplittingTreeNode::getLPrime() const {
    return content.aux.lPrime;
}

SplittingNodeContent& SplittingTreeNode::getContent() {
    return content;
}

int SplittingTreeNode::isDNFTrueOrFalse(const ClauseSet &cs) const {
    if (cs.size() == 0)
        return 1;
    if (cs.size() == 1) {
        ClauseSet::const_iterator first = cs.begin();
        if ((*first)->size() == 0)
            return 2;
    }
    return 0;
}

}
